Nuprl Lemma : safety_induced
4,23
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
P
:((
B
List)
Prop). safety(
B
;
L
.
P
(
L
))
safety(
A
;
L
.
P
(map(
f
;
L
)))
latex
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
l1
l2
,
x
(
s
)
,
map(
f
;
as
)
,
t
T
,
Prop
,
safety(
A
;
tr
.
P
(
tr
))
Lemmas
iseg
wf
,
map
wf
,
iseg
map
origin
A, B:Type, f:(A
B), P:((B List)Prop). safety(B;L.P(L)) 
safety(A;L.P(map(f;L))) A, B:Type, f:(AB), P:((B List)Prop). safety(B;L.P(L)) safety(A;L.P(map(f;L))) Qx:A. B(x)
l2
T